Nuprl Lemma : map_id
11,40
postcript
pdf
A
:Type,
as
:(
A
List). map(Id{
A
};
as
) =
as
latex
Definitions
t
T
,
Id
,
Y
,
Id{
T
}
,
map(
f
;
as
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
Lemmas
rev
implies
wf
,
iff
wf
origin
A:Type, as:(A List). map(Id{A};as) = as A:Type, as:(A List). map(Id{A};as) = as 
Tx:A. B(x)
Q
Q Q